| Definitions | e   X, pred(e), first(e), suptype(S; T), S  T,  x:A.B(x), pred!(e;e'), SWellFounded(R(x;y)), constant_function(f;A;B), r  s, val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time),  , Msg(M), kind(e), loc(e), kindcase(k; a.f(a); l,t.g(l;t) ), EOrderAxioms(E; pred?; info), Unit, EqDecider(T),  , EState(T), sys-order(es; Sys; f),   x,y. t(x;y), retraction(T;f), x. t(x), {T}, x.A(x), locl(a), P   Q, P  Q, a = b, Knd, IdLnk, pred(e), A c B, (last change to x before e), @e(x v),  e(e1,e2].P(e), X(e), Atom$n, (e < e'), e < e', loc(e), t.1, let x,y = A in B(x;y), (e <loc e'), y=f*(x) via L,  , y is f*(x), Top, False, !Void(), no_repeats(T;l), (x l), adjacent(T;L;x;y), L1 L2, hd(l), P & Q, a < b,  x:A. B(x), e loc e' , P  Q, left + right,  b, x:A  B(x), <a, b>,  , AbsInterface(A), Type, ES, P Q, strong-subtype(A;B), a:A fp B(a), sys-antecedent(es;Sys), {x:A| B(x)} , chain-consistent(f;chain), type List, Id, E, fifo-antecedent(es;Sys;f), x:A. B(x), x:A B(x), e c e', f(a),  A, E(X), s = t, t T, last(L), lastchange(x;e), isrcv(k), es-first-from(es;e;l;tg), isrcv(e), s ~ t, SQType(T), es-init(es;e), destination(l), source(l), if b then t else f fi , case b of inl(x) => s(x) | inr(y) => t(y), first(e), kind(e), Dec(P), f**(e), e(e1,e2].P(e), e[e1,e2].P(e), e[e1,e2].P(e), e[e1,e2).P(e), e[e1,e2).P(e), ee'.P(e), e<e'. P(e), ee'.P(e), e<e'.P(e), MaName, l_disjoint(T;l1;l2), t ...$L, True,  T, x << y, x <<= y, as @ bs, increasing(f;k), #$n, ||as||, f(x)?z, f g, IsPrimeIdeal(R;P), IsIntegDom(r), a b, IsMonHom{M1,M2}(f), IsGroup(T;op;id;inv), IsMonoid(T;op;id), monot(T;x,y.R(x;y);f), Cancel(T;S;op), FunThru2op(A;B;opa;opb;f), fun_thru_1op(A;B;opa;opb;f), Dist1op2opLR(A;1op;2op), IsAction(A;x;e;S;f), IsBilinear(A;B;C;+a;+b;+c;f), BiLinear(T;pl;tm), Inverse(T;op;id;inv), Comm(T;op), Assoc(T;op), Ident(T;op;id), CoPrime(a,b), Connex(T;x,y.R(x;y)), AntiSym(T;x,y.R(x;y)), Trans(T;x,y.E(x;y)), Sym(T;x,y.E(x;y)), Refl(T;x,y.E(x;y)), IsEqFun(T;eq), Inj(A;B;f), InvFuns(A;B;f;g), a =!x:T. Q(x), SqStable(P), Outcome, q-rel(r;x), r < s, (xL.P(x)), xL. P(x), x f y, a < b, a <p b, a b, a ~ b, b | a, inl x , tt, inr x , ff, ecase1(e;info;i.f(i);l,e'.g(l;e')), pi2(t), es_info(es), R^+,  ,  , rel_exp(T; R; n), Y, (i = j), int_eq(a; b; c; d), n - m, b, isl(x), outl(x), token{$token:t}, rcv?(e), sender(e),  , Ax, es-pred?(es), link(e), A B, x,y:A//B(x;y), b-union(A; B), int_nzero, nequal(T; a; b), qeq(r;s), isint(z; a; b), multiply(n; m), islocal(k), rcv(l; tg), actof(k), outr(x), state_when(e; info; pred?; init; Trans; val; time), when-after(e; info; pred?; init; Trans; val; time), let(a; x.b(x)), es-shift(s; r), qadd(r; s), n+m, qsub(r; s), qmul(r; s), -n, rec-case(a) of [] => s | x::y => z.t(x;y;z), l[i], nth_tl(n;as), i z j, i <z j, if a<b then c else d, tl(l), lnk(k), tagof(k), grp_le(g), qadd_grp, q_le(r;s), p q, qpositive(r), p q, can-apply(f;x), cr-fails-before(es; Sys; chain; x; y), x before y l, {i..j }, A List, [car / cdr], [], i j < k |
| Lemmas | chain-order-antireflexive, adjacent-to-same-sublist2, chain-order-le transitivity, chain-order-antisymmetric, le wf, int seg wf, length wf1, select wf, length wf nat, increasing wf, adjacent-to-same-sublist, sublist weakening, chain-pullback, chain-order transitivity, chain-consistent-fails-before2, chain-order-le wf, chain-order wf, l before wf, cr-fails-before wf, chain-consistent-monotone-lemma0, chain-order-total2, es-locl-antireflexive, bfalse wf, btrue wf, decidable assert, sq stable from decidable, adjacent wf, and functionality wrt iff, sublist wf, chain-path-ordered, es-locl irreflexivity, fun-connected-step-back, fun-connected weakening eq, es-le weakening eq, es-locl transitivity1, es-first wf, squash wf, true wf, fifo-antecedent-order-preserving, decidable equal Id, chain-path-ordered-same-loc3, es-le-not-locl, decidable es-locl, fun-connected transitivity, decidable equal es-E-interface, fun-connected-step, fun-connected-induction, es-locl transitivity2, es-causl weakening, es-locl-iff, es-loc-pred, es-le wf, es-le-loc, Id sq, guard wf, es-isrcv-loc, chain-path-ordered-same-loc, subtype rel wf, sys-antecedent wf, es-E-interface wf, member wf, fun-connected wf, fun-path wf, es-E wf, es-locl wf, es-causl wf, Id wf, es-loc wf, not wf, false wf, assert-eq-id, assert wf, rev implies wf, iff wf, eq id wf, implies functionality wrt iff, all functionality wrt iff, sys-antecedent-retraction, strong-fun-connected-induction, event system wf, EState wf, rationals wf, strongwellfounded wf, pred! wf, unit wf, top wf, first wf, loc wf, constant function wf, IdLnk wf, kindcase wf, Knd wf, bool wf, qle wf, cless wf, val-axiom wf, nat wf, Msg wf, kind wf, EOrderAxioms wf, deq wf, es-is-interface wf, es-interface wf, es-causle wf, fifo-antecedent wf, es-E-interface-subtype rel, chain-consistent wf, sys-order wf |
